;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
; Interface for the trade increase module

(interface Itradeincrease
  (sig tradeincrease (ticker start end tree))
  (sig tradeincrease-query (start end tickers tree))
  
  (con tradeincrease-string
       (implies (and (stringp ticker)
                (natp start)
                (natp end))
                (equal t (stringp (car (tradeincrease (ticker start end tree)))))))
  
  (con tradeincrease-integer1
       (implies (and (stringp ticker)
                (natp start)
                (natp end))
                (equal t (natp (cadr (tradeincrease (ticker start end tree)))))))
  
  (con tradeincrease-query-string
       (implies (and (natp start)
                     (natp end)
                     (consp tickers))
       (equal t (stringp (tradeincrease-query (start end tickers tree)))))))
